Inference at * 1 1 
Iof proof for Lemma btrue neq bfalse:



1. tt = ff
2. if tt then 1 else 0 fi  = if ff then 1 else 0 fi 
  False 

latex

 by ((RWH ifthenelse_evalC 2) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n
C),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions

False, if b then t else f fi , ff, tt